DROPS

Document

DOI: 10.4230/LIPIcs.CSL.2023.5

A Cyclic Proof System for Full Computation Tree Logic

Authors: Bahareh Afshari, Graham E. Leigh, and Guillermo Menéndez Turata

Published in: LIPIcs, Volume 252, 31st EACSL Annual Conference on Computer Science Logic (CSL 2023)

Abstract

Full Computation Tree Logic, commonly denoted CTL*, is the extension of Linear Temporal Logic LTL by path quantification for reasoning about branching time. In contrast to traditional Computation Tree Logic CTL, the path quantifiers are not bound to specific linear modalities, resulting in a more expressive language. We present a sound and complete hypersequent calculus for CTL*. The proof system is cyclic in the sense that proofs are finite derivation trees with back-edges. A syntactic success condition on non-axiomatic leaves guarantees soundness. Completeness is established by relating cyclic proofs to a natural ill-founded sequent calculus for the logic.

Cite as

Bahareh Afshari, Graham E. Leigh, and Guillermo Menéndez Turata. A Cyclic Proof System for Full Computation Tree Logic. In 31st EACSL Annual Conference on Computer Science Logic (CSL 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 252, pp. 5:1-5:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{afshari_et_al:LIPIcs.CSL.2023.5,
  author =	{Afshari, Bahareh and Leigh, Graham E. and Men\'{e}ndez Turata, Guillermo},
  title =	{{A Cyclic Proof System for Full Computation Tree Logic}},
  booktitle =	{31st EACSL Annual Conference on Computer Science Logic (CSL 2023)},
  pages =	{5:1--5:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-264-8},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{252},
  editor =	{Klin, Bartek and Pimentel, Elaine},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CSL.2023.5},
  URN =		{urn:nbn:de:0030-drops-174664},
  doi =		{10.4230/LIPIcs.CSL.2023.5},
  annote =	{Keywords: Full computation tree logic, Hypersequent calculus, Cyclic proofs}
}

Search Results

Documents authored by Menéndez Turata, Guillermo

A Cyclic Proof System for Full Computation Tree Logic

Abstract

Cite as

Thanks for your feedback!

Could not send message